Nuprl Definition : nat_plus
13,42
postcript
pdf
== {
i
:
| 0 <
i
}
latex
Up
int
1
,
int
1
Wellformedness Lemmas
nat
plus
wf
,
nat
plus
wf
Definitions
{
x
:
A
|
B
(
x
)}
,
,
a
<
b
,
#$n
FDL editor aliases
nat_plus
origin
== {i:
| 0 < i} == {i:| 0 < i}